(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE(i1, t1, e1), F) → False
eqExp(ITE(i1, t1, e1), T) → False
eqExp(ITE(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE(i1, t1, e1), ITE(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE(i1, t1, e1), F) → False
checkConstrExp(ITE(i1, t1, e1), T) → False
checkConstrExp(ITE(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE(i1, t1, e1), ITE(i2, t2, e2)) → True
checkConstrExp(ITE(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE(i, t, e)) → t
getIfGuard(ITE(i, t, e)) → i
getIfFalse(ITE(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
The (relative) TRS S consists of the following rules:
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
eeval(Fun(0, e), ns, vs, Cons(Fun(0, e1073_3), xs1074_3)) →+ eeval[Let][Let][Let](Fun(0, e), ns, vs, Cons(Fun(0, e1073_3), xs1074_3), e1073_3, 0, eeval(e, ns, vs, Cons(Fun(0, e1073_3), xs1074_3)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [6].
The pumping substitution is [e / Fun(0, e)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)